Section 11.1 in [Lucas - IC'02]

Summary: ExSec11_1_Luc02a

• CS-TRS format
• OBJ format
• Negative results:
• Positive results:
  1. Lucas' transformation (LPO @ AProVE)
  2. Zantema's transformation (RPOS @ AProVE)
  3. Ferreira and Ribeiro's transformation (Corollary)
  4. Giesl and Middeldorp's transformation (Corollary)
  5. CSRPO
  6. CSDP

CS-TRS ExSec11_1_Luc02a (file ExSec11_1_Luc02a.csr)

Functions:  terms cons recip sqr s 0 add dbl first nil half

Constructors:  cons recip s 0 nil

Variables:  N X Y Z

Arities: 

ar(terms) = 1
ar(cons) = 2
ar(recip) = 1
ar(sqr) = 1
ar(s) = 1
ar(0) = 0
ar(add) = 2
ar(dbl) = 1
ar(first) = 2
ar(nil) = 0
ar(half) = 1

Replacement map: 

µ(terms)={1}
µ(cons)={1}
µ(recip)={1}
µ(sqr)={1}
µ(s)={1}
µ(0)={}
µ(add)={1,2}
µ(dbl)={1}
µ(first)={1,2}
µ(nil)={}
µ(half)={1}

Rules:  (file ExSec11_1_Luc02a) 

terms(N) -> cons(recip(sqr(N)),terms(s(N)))
sqr(0) -> 0
sqr(s(X)) -> s(add(sqr(X),dbl(X)))
dbl(0) -> 0
dbl(s(X)) -> s(s(dbl(X)))
add(0,X) -> X
add(s(X),Y) -> s(add(X,Y))
first(0,X) -> nil
first(s(X),cons(Y,Z)) -> cons(Y,first(X,Z))
half(0) -> 0
half(s(0)) -> 0
half(s(s(X))) -> s(half(X))
half(dbl(X)) -> X

The CS-TRS in OBJ format (file ExSec11_1_Luc02a.obj):

obj ExSec11_1_Luc02a is
  sort S .
  op terms : S -> S .
  op cons : S S -> S [strat (1 0)] .
  op recip : S -> S .
  op sqr : S -> S .
  op s : S -> S .
  op 0 : -> S .
  op add : S S -> S .
  op dbl : S -> S .
  op first : S S -> S .
  op nil : -> S .
  op half : S -> S .
  vars N X Y Z : S .
  eq terms(N) = cons(recip(sqr(N)),terms(s(N))) .
  eq sqr(0) = 0 .
  eq sqr(s(X)) = s(add(sqr(X),dbl(X))) .
  eq dbl(0) = 0 .
  eq dbl(s(X)) = s(s(dbl(X))) .
  eq add(0,X) = X .
  eq add(s(X),Y) = s(add(X,Y)) .
  eq first(0,X) = nil .
  eq first(s(X),cons(Y,Z)) = cons(Y,first(X,Z)) .
  eq half(0) = 0 .
  eq half(s(0)) = 0 .
  eq half(s(s(X))) = s(half(X)) .
  eq half(dbl(X)) = X .
endo

Negative results

Positive results

1. ExSec11_1_Luc02a is proved µ-terminating in [Luc02a, Section 11.1] by using Lucas's transformation. The TRS ExSec11_1_Luc02a_L:

      terms(N) -> cons(recip(sqr(N)))
      sqr(0) -> 0
      sqr(s(X)) -> s(add(sqr(X),dbl(X)))
      dbl(0) -> 0
      dbl(s(X)) -> s(s(dbl(X)))
      add(0,X) -> X
      add(s(X),Y) -> s(add(X,Y))
      first(0,X) -> nil
      first(s(X),cons(Y)) -> cons(Y)
      half(0) -> 0
      half(s(0)) -> 0
      half(s(s(X))) -> s(half(X))
      half(dbl(X)) -> X
       

   is terminating (use LPO with AProVE).
2. The µ-termination of ExSec11_1_Luc02a can be proved by using Zantema's transformation. The TRS ExSec11_1_Luc02a_Z:

       terms(N) -> cons(recip(sqr(N)),n__terms(s(N)))
       sqr(0) -> 0
       sqr(s(X)) -> s(add(sqr(X),dbl(X)))
       dbl(0) -> 0
       dbl(s(X)) -> s(s(dbl(X)))
       add(0,X) -> X
       add(s(X),Y) -> s(add(X,Y))
       first(0,X) -> nil
       first(s(X),cons(Y,Z)) -> cons(Y,n__first(X,activate(Z)))
       half(0) -> 0
       half(s(0)) -> 0
       half(s(s(X))) -> s(half(X))
       half(dbl(X)) -> X
       terms(X) -> n__terms(X)
       first(X1,X2) -> n__first(X1,X2)
       activate(n__terms(X)) -> terms(X)
       activate(n__first(X1,X2)) -> first(X1,X2)
       activate(X) -> X
       

   is terminating (use RPOS with AProVE).
3. By [GM04, Theorem 11], the µ-termination of ExSec11_1_Luc02a can also be proved by using Ferreira and Ribeiro's transformation (but no concrete proof has been reported yet).
4. By [GM04, Theorem 22], the µ-termination of ExSec11_1_Luc02a can also be proved by using Giesl and Middeldorp's transformation (but no concrete proof has been reported yet).
5. The µ-termination of ExSec11_1_Luc02a can be proved by using CSRPO (proof due to Albert Rubio)and automatically by MuTerm:
   • marking map:

            m(cons,2)={terms}
            

   • precedence:

            terms > cons, recip, sqr, terms', s
            sqr > s, add, dbl
            dbl > s
            add > s
            first > nil, cons, terms
            half > s
            

   • status:

            st(first) = lex
            

6. The µ-termination of ExSec11_1_Luc02a can be proved by using CSDP (computed by MuTerm).